DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2017.30

A Curry-Howard Approach to Church's Synthesis

Authors: Pierre Pradic and Colin Riba

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract

Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, a non-classical subsystem of MSO, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model.

Cite as

Pierre Pradic and Colin Riba. A Curry-Howard Approach to Church's Synthesis. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{pradic_et_al:LIPIcs.FSCD.2017.30,
  author =	{Pradic, Pierre and Riba, Colin},
  title =	{{A Curry-Howard Approach to Church's Synthesis}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.30},
  URN =		{urn:nbn:de:0030-drops-77198},
  doi =		{10.4230/LIPIcs.FSCD.2017.30},
  annote =	{Keywords: Intuitionistic Arithmetic, Realizability, Monadic Second-Order Logic on Infinite Words}
}

Document

DOI: 10.4230/LIPIcs.TLCA.2015.302

Fibrations of Tree Automata

Authors: Colin Riba

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract

We propose a notion of morphisms between tree automata based on game semantics. Morphisms are winning strategies on a synchronous restriction of the linear implication between acceptance games. This leads to split indexed categories, with substitution based on a suitable notion of synchronous tree function. By restricting to tree functions issued from maps on alphabets, this gives a fibration of tree automata. We then discuss the (fibrewise) monoidal structure issued from the synchronous product of automata. We also discuss how a variant of the usual projection operation on automata leads to an existential quantification in the fibered sense. Our notion of morphism is correct (it respects language inclusion), and in a weaker sense also complete.

Cite as

Colin Riba. Fibrations of Tree Automata. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 302-316, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{riba:LIPIcs.TLCA.2015.302,
  author =	{Riba, Colin},
  title =	{{Fibrations of Tree Automata}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{302--316},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.302},
  URN =		{urn:nbn:de:0030-drops-51719},
  doi =		{10.4230/LIPIcs.TLCA.2015.302},
  annote =	{Keywords: Tree automata, Game semantics, Categorical logic.}
}

Search Results

Documents authored by Riba, Colin

A Curry-Howard Approach to Church's Synthesis

Abstract

Cite as

Fibrations of Tree Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message